es:ES.
(e:E.
((timed)state after e = Trans(loc(e))(kind(e),val(e),es_state_when(es;e))  es_state(es;loc(e)))
& (e:E.
& ((islocal(kind(e)))
& ( (n:
& ( (((isl(Choose(loc(e))(act(kind(e)),n,(state when e))))
& ( (c (val(e) = outl(Choose(loc(e))(act(kind(e)),n,(state when e)))  valtype(e)))))
& (e:E.
& ((isrcv(kind(e)))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  Send(loc(sender(e)))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  (kind(sender(e))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  ,val(sender(e))
& ( (<lnk(kind(e)), tag(kind(e)), val(e)>  ,(state when sender(e))))) 

latex

Definitions

x:A  B(x), E, b, , valtype(e), s = t, A c B, x:A. B(x), x:AB(x), P  Q, x:A. B(x), Msg, (x  l), P & Q, es_state(es;i), ES, t  T, es_init(es), es-Trans(es), es_val(es), pred(e), when-after(e;info;pred?;init;Trans;val;time), t.2, es_time(es), f(a), r - s, s+r, kind(e), loc(e), x.A(x), let x = a in b(x), A, b, , , Unit, Void, x:A.B(x), Top, S  T, Type, left + right, suptype(S; T), es-pred?(es), first(e), P  Q, es_state_when(es;e), val(e), Trans(i), (timed)state after e, <a, b>, es_vartype(es;i;x), , es-T(es), Id, True, let x,y = A in B(x;y), t.1, False, e loc e' , isrcv(e), Atom$n, P  Q, T, , Choose(i), (state when e), rcvtype(e), acttype(e), es-Choose(es), x when e, es-M(es), lnk(e), tag(e), es-V(es), act(e), es_info(es), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), if b then t else f fi , Send(i), sender(e), es-Send(es)

Lemmas

islocal-not-isrcv, squash wf, true wf, es-isrcv-loc, es-le-loc, es-loc-pred, Id wf, es init wf, es state wf, es-E wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, first wf, es-pred? wf, top wf, unit wf, bool wf, bnot wf, not wf, assert wf, es-Trans wf, es-loc wf, es-kind wf, es val wf, es-shift wf2, qsub wf, es time wf, es-pred wf, event system wf